/*
 * Atomic Predicates for Transformers
 * 
 * Copyright (c) 2015 UNIVERSITY OF TEXAS AUSTIN. All rights reserved. Developed
 * by: HONGKUN YANG and SIMON S. LAM http://www.cs.utexas.edu/users/lam/NRL/
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * with the Software without restriction, including without limitation the
 * rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
 * sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * 1. Redistributions of source code must retain the above copyright notice,
 * this list of conditions and the following disclaimers.
 * 
 * 2. Redistributions in binary form must reproduce the above copyright notice,
 * this list of conditions and the following disclaimers in the documentation
 * and/or other materials provided with the distribution.
 * 
 * 3. Neither the name of the UNIVERSITY OF TEXAS AUSTIN nor the names of the
 * developers may be used to endorse or promote products derived from this
 * Software without specific prior written permission.
 * 
 * 4. Any report or paper describing results derived from using any part of this
 * Software must cite the following publication of the developers: Hongkun Yang
 * and Simon S. Lam, Scalable Verification of Networks With Packet Transformers
 * Using Atomic Predicates, IEEE/ACM Transactions on Networking, October 2017,
 * Volume 25, No. 5, pages 2900-2915 (first published as IEEE Early Access
 * Article, July 2017, Digital Object Identifier: 10.1109/TNET.2017.2720172).
 * 
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH
 * THE SOFTWARE.
 */
package transformer;

import java.io.*;
import java.util.*;

import common.PositionTuple;

// for graphical representation
public class Node {
	String name;
	ArrayList<Node> children;

	static int node_cnt;

	public Node(String name)
	{
		this.name = name;
	}

	public void addChild(Node n)
	{
		if(children == null)
		{
			children = new ArrayList<Node>();
		}
		children.add(n);
	}

	public void delChild(Node n)
	{
		children.remove(n);
		if(children.isEmpty())
		{
			children = null;
		}
	}
	
	// remove the re-occurance of root
	public static void removeLoop(Node root)
	{
		removeLoop_recur(root, root);
	}

	private static void removeLoop_recur(Node cur_node, Node root)
	{
		if(cur_node.children != null)
		{
			HashSet<Node> to_del = new HashSet<Node>();
			for(Node c : cur_node.children)
			{
				if(c.equals(root))
				{
					to_del.add(c);
				}else
				{
					removeLoop_recur(c, root);
				}
			}
			for(Node d : to_del)
			{
				cur_node.delChild(d);
			}
		}
	}

	public boolean equals(Object o)
	{
		if(((Node)o).name.equals(this.name))
		{
			return true;
		}else
		{
			return false;
		}
	}

	// only store device information
	public static Node convert(AbstractState s)
	{
		Node n = new Node(s.pt.getDeviceName());

		if(s.nextState!= null)
		{
			if(s.nextState.get(0).pt.getDeviceName().equals(n.name))
			{
				for(AbstractState n_s : s.nextState)
				{
					ArrayList<AbstractState> nn_ss = n_s.nextState;
					if(nn_ss != null)
					{
						for(AbstractState nn_s : nn_ss)
						{
							n.addChild(convert(nn_s));
						}
					}
				}

			}else
			{
				for(AbstractState n_s : s.nextState)
				{
					n.addChild(convert(n_s));
				}
			}
		}
		return n;
	}

	/**
	 * depth first print
	 */
	public void print()
	{
		print_recur("");
	}

	public void print_recur(String headstr)
	{
		String newheadstr = headstr + name + "->";
		if(children == null)
		{
			System.out.println(newheadstr);
		}else
		{
			for(int i = 0; i < children.size(); i ++)
			{
				Node nxtN = children.get(i);
				nxtN.print_recur(newheadstr);
			}
		}

	}

	public static void main(String[] args) throws IOException
	{
		plot_tree6(new PositionTuple("kans", "xe-0/1/1"));

	}
	
	public static void plot_tree6(PositionTuple pt) throws IOException
	{
		Network net = new Network("i2", false, true);
		Device.only_v6 = true;
		StateTransfer stfer = new StateTransfer(net);
		StateBDD hs = stfer.TraverseAnyPkt(pt);
		hs.printState();
		StateBDD.removeLoop(hs);
		Node n = Node.convert(hs);
		//Node.removeLoop(n);
		n.draw(new PrintWriter("v6" + pt.getDeviceName() + ".dot"), "v6tree");
	}
	
	/**
	 * for mpls tree and non-mpls tree
	 * @param pt = new PositionTuple("kans", "xe-0/1/1")
	 * @throws IOException
	 */
	public static void plot_tree(PositionTuple pt) throws IOException
	{
		Network net = new Network("i2", true);
		StateTransfer stfer = new StateTransfer(net);

		StateBDD hs = stfer.TraverseCombPkt(pt);
		//State hs = stfer.TraverseAnyPkt(new PositionTuple("kans", "xe-0/1/1"));
		hs.printState();
		StateBDD.removeLoop(hs);
		Node n = Node.convert(hs);
		Node.removeLoop(n);
		n.draw(new PrintWriter("mpls.dot"), "mpls");
		//Node.convert(hs).print();
	}

	// generate dot file
	public void draw(PrintWriter pw, String graph_name)
	{
		pw.println("digraph " + graph_name + " {");
		pw.println("node [fontname=Arial, fontsize=16, margin=0,shape=circle];");
		pw.println("rankdir=LR;");
		node_cnt = 0;
		String node_id = "n"+node_cnt;
		pw.println(node_def(node_cnt));

		if(children != null)
		{
			for(Node c:children)
			{
				c.draw_recur(pw, node_id);
			}
		}

		pw.println("}");
		pw.close();
	}

	private void draw_recur(PrintWriter pw, String parent)
	{
		node_cnt ++;
		pw.println(node_def(node_cnt));
		String node_id = "n"+node_cnt;
		pw.println(parent+"->"+node_id);
		if(children != null)
		{
			for(Node c:children)
			{
				c.draw_recur(pw, node_id);
			}
		}
	}

	private String node_def(int id)
	{
		String name_str = name;
		if(name.length() > 4)
		{
			name_str = name.substring(0, 4);
		}
		return "n" + id+" [label=" + name_str + "]";
	}

	/*
	  digraph BST {
    node [fontname=Arial, fontsize=16, margin=0,0,shape=circle];
    rankdir=LR;
    15 -> 6;
    null0 [label=atla];
    6 -> null0;
    null1 [shape=point];
    6 -> null1;
    15 -> 18;
    18 -> 17;
    null2 [shape=point];
    17 -> null2;
    null3 [shape=point];
    17 -> null3;
    null4 [shape=point];
    18 -> null4;
}
	 */

}
